\documentclass[conference]{IEEEtran}

\usepackage[cmex10]{amsmath}
\usepackage[tight,style=math]{k}
\usepackage{graphicx}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{wrapfig}
\usepackage{multirow}
\usepackage{caption}
\usepackage{alltt}

\newcommand{\eqbydef}{\triangleq}
\newcommand{\IMP}{\textsc{IMP}\xspace}
\newcommand{\Ra}{\pmb{\Rightarrow}}
\newcommand{\true}{\mathit{true}}
\newcommand{\false}{\mathit{false}}
\renewcommand{\S}{\mathcal{A}}
\newcommand{\C}{\mathcal{C}}
\newcommand{\Var}{\mathit{Var}}
\newcommand{\Bool}{\mathit{Bool}}
\newcommand{\Cfg}{\mathit{Cfg}}
\newcommand{\T}{\mathcal{T}}
\newcommand{\pattern}[2]{{#1}%
  \ifthenelse{\equal{#2}{}}{}{%
    \pmb{\wedge}{#2}%
  }%
}
\renewcommand{\terminal}[1]{\fontsize{8}{10}\selectfont \text{ }{\tt #1}\text{ }}
\newcommand{\mytt}[1]{{\fontsize{9}{11}\selectfont{$\mathtt{#1}$}}}
\newcommand{\myttt}[1]{{\fontsize{8}{10}\selectfont{$\mathtt{#1}$}}}
\newcommand{\sm}[1]{\fontsize{8}{10}\selectfont {#1}}
%\newcommand{\mytt}[1]{$\text{\ttfamily #1}$}


\newcommand{\htriple}[3]{\{{#1}\}{#2}\{{#3}\}}

\newcommand{\rrule}[3]{{#1}%
  \ifthenelse{\equal{#3}{}}{}{%
    \pmb{\wedge}{#3}%
  }%
  \pmb{\Rightarrow}{#2}
}


\newcommand{\tbd}[1]{\par\noindent {\color{red} #1}\\ }

\newcommand{\ax}[1]{{\fontsize{8}{9}\selectfont\textbf{#1}}}
\newcommand{\step}[1]{{\textbf{#1}}}

\renewcommand{\textfraction}{0.05}
\renewcommand{\topfraction}{0.95}
\renewcommand{\bottomfraction}{0.95}
\renewcommand{\floatpagefraction}{0.35}
\setcounter{totalnumber}{5}

\ifCLASSINFOpdf
\else
\fi





% *** MATH PACKAGES ***
%
% A popular package from the American Mathematical Society that provides
% many useful and powerful commands for dealing with mathematics. If using
% it, be sure to load this package with the cmex10 option to ensure that
% only type 1 fonts will utilized at all point sizes. Without this option,
% it is possible that some math symbols, particularly those within
% footnotes, will be rendered in bitmap form which will result in a
% document that can not be IEEE Xplore compliant!
%
% Also, note that the amsmath package sets \interdisplaylinepenalty to 10000
% thus preventing page breaks from occurring within multiline equations. Use:
%\interdisplaylinepenalty=2500
% after loading amsmath to restore such page breaks as IEEEtran.cls normally
% does. amsmath.sty is already installed on most LaTeX systems. The latest
% version and documentation can be obtained at:
% http://www.ctan.org/tex-archive/macros/latex/required/amslatex/math/

%\newcounter{def}

\newtheoremstyle{mystyle}%                % Name
  {}%                                     % Space above
  {}%                                     % Space below
  {\itshape}%                             % Body font
  {}%                                     % Indent amount
  {\bfseries}%                            % Theorem head font
  {.}%                                    % Punctuation after theorem head
  { }%                                    % Space after theorem head, ' ', or \newline
  {}%                                     % Theorem head spec (can be left empty, meaning `normal')

%\theoremstyle{mystyle}

\newtheorem{theorem}{Theorem}%[section]
\newtheorem{definition}{Definition}%[def]
\newtheorem{assumption}{Assumption}
%\newtheorem{proposition}[theorem]{Proposition}
%\newtheorem{corollary}[theorem]{Corollary}

%\newenvironment{proof}[1][Proof]{\begin{trivlist}
%\item[\hskip \labelsep {\bfseries #1}]}{\end{trivlist}}
%\newenvironment{definition}[1][Definition]{\begin{trivlist}
%\item[\hskip \labelsep {\bfseries #1}]}{\end{trivlist}}
%\newenvironment{theorem}[1][Theorem]{\begin{trivlist}
%\item[\hskip \labelsep {\bfseries #1}]}{\end{trivlist}}
%\newenvironment{example}[1][Example]{\begin{trivlist}
%\item[\hskip \labelsep {\bfseries #1}]}{\end{trivlist}}
%\newenvironment{remark}[1][Remark]{\begin{trivlist}
%\item[\hskip \labelsep {\bfseries #1}]}{\end{trivlist}}
%\newenvironment{assumption}[1][Assumption]{\begin{trivlist}
%\item[\hskip \labelsep {\bfseries #1}]}{\end{trivlist}}

%\newcommand{\qed}{\nobreak \ifvmode \relax \else
%      \ifdim\lastskip<1.5em \hskip-\lastskip
%      \hskip1.5em plus0em minus0.5em \fi \nobreak
%      \vrule height0.75em width0.5em depth0.25em\fi}




% *** SPECIALIZED LIST PACKAGES ***
%
%\usepackage{algorithmic}
% algorithmic.sty was written by Peter Williams and Rogerio Brito.
% This package provides an algorithmic environment fo describing algorithms.
% You can use the algorithmic environment in-text or within a figure
% environment to provide for a floating algorithm. Do NOT use the algorithm
% floating environment provided by algorithm.sty (by the same authors) or
% algorithm2e.sty (by Christophe Fiorio) as IEEE does not use dedicated
% algorithm float types and packages that provide these will not provide
% correct IEEE style captions. The latest version and documentation of
% algorithmic.sty can be obtained at:
% http://www.ctan.org/tex-archive/macros/latex/contrib/algorithms/
% There is also a support site at:
% http://algorithms.berlios.de/index.html
% Also of interest may be the (relatively newer and more customizable)
% algorithmicx.sty package by Szasz Janos:
% http://www.ctan.org/tex-archive/macros/latex/contrib/algorithmicx/




% *** ALIGNMENT PACKAGES ***
%
%\usepackage{array}
% Frank Mittelbach's and David Carlisle's array.sty patches and improves
% the standard LaTeX2e array and tabular environments to provide better
% appearance and additional user controls. As the default LaTeX2e table
% generation code is lacking to the point of almost being broken with
% respect to the quality of the end results, all users are strongly
% advised to use an enhanced (at the very least that provided by array.sty)
% set of table tools. array.sty is already installed on most systems. The
% latest version and documentation can be obtained at:
% http://www.ctan.org/tex-archive/macros/latex/required/tools/


%\usepackage{mdwmath}
%\usepackage{mdwtab}
% Also highly recommended is Mark Wooding's extremely powerful MDW tools,
% especially mdwmath.sty and mdwtab.sty which are used to format equations
% and tables, respectively. The MDWtools set is already installed on most
% LaTeX systems. The lastest version and documentation is available at:
% http://www.ctan.org/tex-archive/macros/latex/contrib/mdwtools/


% IEEEtran contains the IEEEeqnarray family of commands that can be used to
% generate multiline equations as well as matrices, tables, etc., of high
% quality.


%\usepackage{eqparbox}
% Also of notable interest is Scott Pakin's eqparbox package for creating
% (automatically sized) equal width boxes - aka "natural width parboxes".
% Available at:
% http://www.ctan.org/tex-archive/macros/latex/contrib/eqparbox/





% *** SUBFIGURE PACKAGES ***
%\usepackage[tight,footnotesize]{subfigure}
% subfigure.sty was written by Steven Douglas Cochran. This package makes it
% easy to put subfigures in your figures. e.g., "Figure 1a and 1b". For IEEE
% work, it is a good idea to load it with the tight package option to reduce
% the amount of white space around the subfigures. subfigure.sty is already
% installed on most LaTeX systems. The latest version and documentation can
% be obtained at:
% http://www.ctan.org/tex-archive/obsolete/macros/latex/contrib/subfigure/
% subfigure.sty has been superceeded by subfig.sty.



%\usepackage[caption=false]{caption}
%\usepackage[font=footnotesize]{subfig}
% subfig.sty, also written by Steven Douglas Cochran, is the modern
% replacement for subfigure.sty. However, subfig.sty requires and
% automatically loads Axel Sommerfeldt's caption.sty which will override
% IEEEtran.cls handling of captions and this will result in nonIEEE style
% figure/table captions. To prevent this problem, be sure and preload
% caption.sty with its "caption=false" package option. This is will preserve
% IEEEtran.cls handing of captions. Version 1.3 (2005/06/28) and later 
% (recommended due to many improvements over 1.2) of subfig.sty supports
% the caption=false option directly:
%\usepackage[caption=false,font=footnotesize]{subfig}
%
% The latest version and documentation can be obtained at:
% http://www.ctan.org/tex-archive/macros/latex/contrib/subfig/
% The latest version and documentation of caption.sty can be obtained at:
% http://www.ctan.org/tex-archive/macros/latex/contrib/caption/




% *** FLOAT PACKAGES ***
%
%\usepackage{fixltx2e}
% fixltx2e, the successor to the earlier fix2col.sty, was written by
% Frank Mittelbach and David Carlisle. This package corrects a few problems
% in the LaTeX2e kernel, the most notable of which is that in current
% LaTeX2e releases, the ordering of single and double column floats is not
% guaranteed to be preserved. Thus, an unpatched LaTeX2e can allow a
% single column figure to be placed prior to an earlier double column
% figure. The latest version and documentation can be found at:
% http://www.ctan.org/tex-archive/macros/latex/base/



%\usepackage{stfloats}
% stfloats.sty was written by Sigitas Tolusis. This package gives LaTeX2e
% the ability to do double column floats at the bottom of the page as well
% as the top. (e.g., "\begin{figure*}[!b]" is not normally possible in
% LaTeX2e). It also provides a command:
%\fnbelowfloat
% to enable the placement of footnotes below bottom floats (the standard
% LaTeX2e kernel puts them above bottom floats). This is an invasive package
% which rewrites many portions of the LaTeX2e float routines. It may not work
% with other packages that modify the LaTeX2e float routines. The latest
% version and documentation can be obtained at:
% http://www.ctan.org/tex-archive/macros/latex/contrib/sttools/
% Documentation is contained in the stfloats.sty comments as well as in the
% presfull.pdf file. Do not use the stfloats baselinefloat ability as IEEE
% does not allow \baselineskip to stretch. Authors submitting work to the
% IEEE should note that IEEE rarely uses double column equations and
% that authors should try to avoid such use. Do not be tempted to use the
% cuted.sty or midfloat.sty packages (also by Sigitas Tolusis) as IEEE does
% not format its papers in such ways.





% *** PDF, URL AND HYPERLINK PACKAGES ***
%
%\usepackage{url}
% url.sty was written by Donald Arseneau. It provides better support for
% handling and breaking URLs. url.sty is already installed on most LaTeX
% systems. The latest version can be obtained at:
% http://www.ctan.org/tex-archive/macros/latex/contrib/misc/
% Read the url.sty source comments for usage information. Basically,
% \url{my_url_here}.

 \usepackage{algpseudocode}
\usepackage[options]{algorithm}


\newenvironment{mylisting}
{\begin{list}{}{\setlength{\leftmargin}{1em}}\item\scriptsize\bfseries}
{\end{list}}


\begin{document}
%
% paper title
% can use linebreaks \\ within to get better formatting as desired
\title{Engineering Hoare Logic-based\\Program Verification
in K Framework}


% author names and affiliations
% use a multiple column layout for up to three different
% affiliations
\author{
\IEEEauthorblockN{Andrei Arusoaie}
\IEEEauthorblockA{Faculty of Computer Science\\
University of Alexandru Ioan Cuza, Ia{\c s}i\\
Email: andrei.arusoaie@gmail.com
}}

% conference papers do not typically use \thanks and this command
% is locked out in conference mode. If really needed, such as for
% the acknowledgment of grants, issue a \IEEEoverridecommandlockouts
% after \documentclass

% for over three affiliations, or if they all won't fit within the width
% of the page, use this alternative format:
% 
%\author{\IEEEauthorblockN{Michael Shell\IEEEauthorrefmark{1},
%Homer Simpson\IEEEauthorrefmark{2},
%James Kirk\IEEEauthorrefmark{3}, 
%Montgomery Scott\IEEEauthorrefmark{3} and
%Eldon Tyrell\IEEEauthorrefmark{4}}
%\IEEEauthorblockA{\IEEEauthorrefmark{1}School of Electrical and Computer Engineering\\
%Georgia Institute of Technology,
%Atlanta, Georgia 30332--0250\\ Email: see http://www.michaelshell.org/contact.html}
%\IEEEauthorblockA{\IEEEauthorrefmark{2}Twentieth Century Fox, Springfield, USA\\
%Email: homer@thesimpsons.com}
%\IEEEauthorblockA{\IEEEauthorrefmark{3}Starfleet Academy, San Francisco, California 96678-2391\\
%Telephone: (800) 555--1212, Fax: (888) 555--1212}
%\IEEEauthorblockA{\IEEEauthorrefmark{4}Tyrell Inc., 123 Replicant Street, Los Angeles, California 90210--4321}}




% use for special paper notices
%\IEEEspecialpapernotice{(Invited Paper)}




% make the title area
\maketitle


\begin{abstract}
In this paper we describe a methodology for easy development of Hoare Logic verification tools using the \K (operational) semantics of programming languages. %From a theoretical point of view, the approach uses the relationship between Matching  Logic reachability and Hoare Logic, that is, Hoare triples can be transformed into Matching Logic specifications (reachability rules). In previous work we proposed a 
%language independent 
%symbolic execution framework, which we prove here that it can derive reachability rules. Thus, we can transform Hoare triples into reachability rules and then prove them using symbolic execution.
We exploit the relationship between the Hoare Logic and Matching Logic Reachability,
which allows us to translate Hoare triples into reachability rules. Then we use the symbolic
execution support to check the derived reachability rules.
A Hoare triple holds w.r.t. the partial correctness if and only if the execution of its
reachability rule is successful.

The methodology consists in enriching the operational semantics of a programming language with syntax and semantics for additional constructs required when using Hoare Logic. The obtained semantics is then used by the \K Framework to verify annotated programs. 
We instantiate our methodology on a simple imperative language, by describing each step separately, and then we test the obtained tool over the KeY-Hoare tests suite.%~\vspace{2ex}
\end{abstract}
\IEEEpeerreviewmaketitle


\section{Introduction}
Hoare Logic~\cite{DBLP:journals/cacm/Hoare69} or Floyd-Hoare Logic is probably the most popular formal system for reasoning about the correctness of computer programs. Proposed in 1969 by C. A. R. Hoare, the logic was inspired from the work of R. Floyd on flowcharts~\cite{FLOYD67}, and it consists in a set of deduction rules which prove the validity of Hoare triples. Triples are formulas  of the form $\{\psi\}St\{\psi'\}$ representing program properties. $St$ is a piece of code (statements),  $\psi$ and $\psi'$ are assertions,  named {\it precondition} and {\it postcondition}, respectively. Such formulas have the following semantics: a triple holds w.r.t. the partial correctness if and only if any terminating execution of $St$ starting in a state satisfying the precondition $\psi$ ends into a state satisfying the postcondition $\psi'$. If further the precondition ensures the termination of $St$, then $\{\psi\}St\{\psi'\}$ holds w.r.t. total correctness.

The Hoare Logic deduction system is a set of rules used to prove the correctness of Hoare triples w.r.t. partial correctness. The system depends on the language syntax, thus, it needs to be proved sound for each language separately. 
%An approach which eliminates this inconvenience is Matching Logic, which provides a language-independent and a sound proof system which uses the operational semantics of a programming language. 
In~\cite{rosu-stefanescu-2012-fm}, the authors present and prove correct a technique to mechanically translate Hoare logic triples into {\it reachability rules} and Hoare logic proof derivations into equivalent Matching Logic Reachability (MLR) proof derivations.
The main advantage is given by the fact that MLR can be defined independent of language.
Program properties are specified as reachability rules $\varphi \Rightarrow  \varphi'$, where $\varphi$ and $\varphi'$ are {\it patterns}. Patterns are program configuration terms with variables, which contain both program and state, like in the operational semantics. In addition to that, patterns also allow constraints over variables like in Hoare logic. A reachability rule $\varphi \Rightarrow  \varphi'$ states that a program configuration $\gamma$ which {\it matches} $\varphi$ takes zero, one or more steps in the associated transition system to reach a configuration $\gamma'$ that {\it matches} $\varphi'$. The verification of a program reduces to checking if the specification (a reachability rule) is derivable using the deduction rules from the proof system. 

In previous work~\cite{arusoaie:hal-00766220} we proposed a language-independent framework for symbolic execution which applies some transformations on the operational semantics of a language (given as set of rewrite rules), such that programs can be executed with symbolic values. The transformation has been defined formally, and we have proved results regarding the relationship between concrete and symbolic executions. Our symbolic execution framework has been integrated in the \K framework and tested on existing \K language definitions.\vspace{1ex}

In this paper we propose a methodology to turn the \K framework into a Hoare Logic verification tool using the \K operational semantics of the target language. The approach is based on the translation of Hoare triples $\{\psi\}St\{\psi'\}$ into reachability rules $\varphi \Rightarrow \varphi'$, which is described in ~\cite{rosu-stefanescu-2012-fm}.
The resulted reachability rules are checked using the symbolic execution framework  and the Z3 SMT solver~\cite{DBLP:conf/tacas/MouraB08}.
The set of reachability rules is automatically derived during the symbolic execution from the annotated programs.
Our methodology applies directly to the \K semantics of a language. It mainly consists in extending the language syntax with Hoare-like assertions and program annotations, and adding to the language semantics the rewrite rules corresponding to the new annotated statements and to the verification of the reachability rules.
Since the user is in charge of dealing with language specific settings, the methodology remains parametric in the operational semantics. However, the effort made for getting Hoare logic verifier for a given such semantics is minimal.~\vspace{1ex}

\noindent{\bf Motivation}. The \K tool~\cite{lazar-arusoaie-serbanuta-ellison-mereuta-lucanu-rosu-2012-fm} is a system for formally defining programming languages. Formal definitions created using \K, automatically yield an interpreter for the language. In order to enrich its analysis capabilities we proposed a symbolic execution framework~\cite{arusoaie:hal-00766220}, which has been integrated in \K. Therefore, we are able to run programs manipulating symbolic data. 
Our goal is to describe a methodology for extending the \K language definition
such that the verification of Hoare triples is possible with a minimal effort. Since \K started to be used in teaching programming languages design in various universities, the methodology is useful to show how language definitions can be extended with Hoare-like analysis means.

To our best knowledge, there are only a few notable Hoare Logic verification tools based on the formal semantics of a language (e.g. Caduceus~\cite{DBLP:conf/arith/BoldoF07}, Java-ITP~\cite{Sasse:2007:JVT:1279349.1279449}, KeY-Hoare~\cite{Key-Hoare}, Spec\#~\cite{Barnett:2004:SPS:2131546.2131549}). Unfortunately, all these tools are  designed and optimized to work on a specific language. Others (e.g. ITS~\cite{ITS}, JAlgo~\cite{JAlgo}) are not even based on formal definitions of programming languages. A major problem of these tools is that they are not easy to extend or to adapt such that they can be used for verifying programs of a different language. On the other hand, here we propose a methodology that allows users to easily create their own verification tool on top of the operational semantics of a language. Moreover, they can perform program verification using the same tool that runs the semantics (the \K tool).~\vspace{1ex}

\noindent{\bf Contributions.}
The main contributions of this paper are:

\begin{itemize}
\item We present a methodology that applied to the \K semantics of a programming language yields a Hoare Logic verifier for programs of that language. Hoare triples are represented as annotated programs and the semantics of the language is extended, such that during the symbolic execution of the annotated program, a set of reachability rules is automatically derived and proved correct. The validity of Hoare triples is then given by the validity of the reachability rules.

\item We prove that our extended symbolic execution framework derives a valid set of reachability rules for a given pattern.
%\item We provide tool support consisting in an interface for Hoare-like program annotations;
\item We instantiate our methodology on a simple imperative language, called \IMP, and we successfully verified all the programs from the KeY-Hoare
%~\cite{Key-Hoare} 
tests suite. We compared the verification time of each program when using our tool, KeY-Hoare, and Spec\#
%~\cite{Barnett:2004:SPS:2131546.2131549}
.~\vspace{1ex}
\end{itemize}

The rest of the paper is organized as follows. Section~\ref{sec:imp} presents the \K syntax and the semantics of a simple imperative language, intensively used in research papers, called \IMP. In Section~\ref{sec:all} we present the Hoare Logic and Matching Logic basic notions and notations that we are going to use in the paper. At the end of the section we recall the transformation of Hoare triples into reachability rules. In Section~\ref{sec:proof} we prove that symbolic execution derives a valid set of reachability rules. Section~\ref{sec:methodology} contains a detailed description of our methodology by instantiating it on the semantics of \IMP, and we show how the obtained semantics is used for proving and \IMP program. Then, the generated verification tool is compared to existing tools (KeY-Hoare and Spec\#).  In Section~\ref{sec:comparison} we present some related work and we conclude in Section~\ref{sec:conclusions}.

\section{\IMP}
\label{sec:imp}



Our running example is \IMP, a simple imperative language intensively used in research papers. Its syntax is shown in Figure~\ref{imp:syn} and is mostly self explanatory since it uses a BNF notation. The \IMP statements are either assignments, if statements, while loops, skip (i.e., the empty statement), or a list of statements. The attribute {\it strict} in some productions means that the arguments of the annotated expression/statement are evaluated before the expression/statement itself. If the attribute is followed by a list of natural numbers then it only concerns the arguments whose positions are present in the list.

\begin{figure}[t]
%\fontsize{9}{11}
%\selectfont
\begin{center}
\begin{tabular}{ll}
\hline
\multicolumn{2}{l}{
$\begin{array}{ll}
\sort{Id} &::= \textrm{domain of identifiers}\\
\sort{Int} &::= \textrm{domain of integers  (including operations)}\\
\sort{Bool~} &::= \textrm{domain of booleans (including operations)}
\end{array}$
}\\
$
\begin{aligned}
{\nonTerminal{\sort{AExp}}} ::&\!={{\nonTerminal{\sort{Int}}}}\\
&\mid{{\nonTerminal{\sort{Id}}}}{}\\
&\mid{{{\nonTerminal{\sort{AExp}}}}{\terminal{/}}{{\nonTerminal{\sort{AExp}}}}}~[\textrm{strict}]\\
&\mid{{{\nonTerminal{\sort{AExp}}}}{\terminal{*}}{{\nonTerminal{\sort{AExp}}}}}~[\textrm{strict}]\\
&\mid{{{\nonTerminal{\sort{AExp}}}}{\terminal{+}}{{\nonTerminal{\sort{AExp}}}}}~[\textrm{strict}]\\
&\mid{({\nonTerminal{\sort{AExp}}})}{}\\
\end{aligned}
$
&~\\
%\hspace{-6ex}
$
\begin{aligned}
{\sort{BExp}}::&\!={{\nonTerminal{\sort{Bool}}}}{}\\
&\mid
{{{\nonTerminal{\sort{AExp}}}}{\terminal{<=}}{{\nonTerminal{\sort{AExp}}}}}~[\textrm{strict}]\\
&\mid
{{\terminal{not}}{{\nonTerminal{\sort{BExp}}}}}~[\textrm{strict}]\\
&\mid
{{{\nonTerminal{\sort{BExp}}}}{\terminal{and}}{{\nonTerminal{\sort{BExp}}}}}~[\textrm{strict}(1)]\\
&\mid
{({\nonTerminal{\sort{BExp}}})}{}
\end{aligned}
$
\\
$
\begin{aligned}
{\nonTerminal{\sort{Stmt}}}::&\!={{\terminal{skip}}}{}\\
&\mid
{{{\nonTerminal{\sort{Id}}}}{\terminal{:=}}{{\nonTerminal{\sort{AExp}}}}}{}\\
&\mid
{{\terminal{if}}{{\nonTerminal{\sort{BExp}}}}{\terminal{}}{{\nonTerminal{\sort{Stmt}}}}{\terminal{else}}{{\nonTerminal{\sort{Stmt}}}}}~[\textrm{strict}(1)]\\
%\end{aligned}
%$
%&~\\
%$
%\begin{aligned}
&\mid
{{\terminal{\{}}{\nonTerminal{\sort{Stmt}}}{\terminal{\}}}}{}\\
&\mid
{{\terminal{while}}{{\nonTerminal{\sort{BExp}}}}{\terminal{do}}{{\nonTerminal{\sort{Stmt}}}}}{}\\
&\mid
{{{\nonTerminal{\sort{Stmt}}}}{\terminal{;}}{{\nonTerminal{\sort{Stmt}}}}}{}\\
\end{aligned}
$\\
$
\begin{aligned}
%\multicolumn{2}{l}{
\sort{Code}::&\!=\sort{Id}\mid\sort{Int}\mid\sort{Bool}\mid\sort{AExp}\\
&\mid\sort{BExp}\mid\sort{Stmt}\mid \sort{Code}\kra\sort{Code}\\
%}
\end{aligned}
$\\
\hline
\end{tabular}
\end{center}
\caption{\label{imp:syn}\K Syntax of IMP}
\end{figure}


The operational semantics of \IMP consists in a set of rewrite rules, which can also be conditional. These rules are applied to {\it configurations}, which are terms containing the program to be executed and additional information required for program execution. The configuration structure depends on the language being defined; for \IMP, it consists only of the program to be executed and an environment mapping variables to values. In \K,\xspace {\it \xspace configurations} are written as nested structures of cells. For \IMP it consists in a top cell {\it cfg}, having a subcell {\it k} containing the code and a subcell {\it env} containing the environment (cf. Figure ~\ref{imp:cfg}). 

\begin{figure}[b]
\centering
\begin{tabular}{c}
%\hline
$
\begin{array}{ll}
\sort{Cfg}&::=\kall[black]{cfg}{\kall[black]{k}{\sort{Code}}\kall[black]{env}{\sort{Map}_{\mathit{Id},\mathit{Int}}}}
\end{array}
$
%~\\\hline
\end{tabular}~\vspace{2ex}
\caption{\label{imp:cfg}\K Configuration of IMP}
\end{figure}



The code inside the {\it k} cell is represented as a list of computation tasks $C_1 \kra C_2 \kra \ldots \kra C_n$ to be executed in the given order. Computation tasks are typically statements and expressions. The environment in the {\it env} cell is a map containing bindings of identifiers to values, e.g., $a \mapsto 3 \text{ } b \mapsto 1$.

The semantics of \IMP is shown in  Figure~\ref{imp:sem}.  Each rewrite rule from the semantics specifies how the configuration evolves when the first computation task from the $\terminal{k}$ cell is executed. The three dots in a cell mean that the rest of the cell remains unchanged. Most syntactical constructions require only one semantical rule. The exceptions are the conjunction operation  and the $\terminal{if}$ statement,  which have  Boolean arguments and require two rules each (one rule per Boolean value).

\begin{figure}[t]
\hspace{-0.5ex}\begin{minipage}{.48\textwidth}
\hrule
\begin{center}
$
\begin{aligned}
&\rrule{\kprefix[black]{cfg}{\kprefix[black]{k}{I_1\terminal{+}I_2}}}
{\kprefix[black]{cfg}{\kprefix[black]{k}{I_1+_{\mathit{Int}}I_2}}}{}\\
&\rrule{\kprefix[black]{cfg}{\kprefix[black]{k}{I_1\terminal{*}I_2}}}
{\kprefix[black]{cfg}{\kprefix[black]{k}{I_1*_{\mathit{Int}}I_2}}}{}\\
&\rrule{\kprefix[black]{cfg}{\kprefix[black]{k}{I_1\terminal{/}I_2}}}
{\kprefix[black]{cfg}{\kprefix[black]{k}{I_1/_{\mathit{Int}}I_2}}}{I_2\not=_\mathit{Int}0}\\
&\rrule{\kprefix[black]{cfg}{\kprefix[black]{k}{I_1\terminal{<=}I_2}}}
{\kprefix[black]{cfg}{\kprefix[black]{k}{I_1\le_{\mathit{Int}}I_2}}}{}\\
&\rrule{\kprefix[black]{cfg}{\kprefix[black]{k}{\true\terminal{and}B}}}
{\kprefix[black]{cfg}{\kprefix[black]{k}{B}}}{}\\
&\rrule{\kprefix[black]{cfg}{\kprefix[black]{k}{\false\terminal{and}B}}}
{\kprefix[black]{cfg}{\kprefix[black]{k}{\false}}}{}\\
&\rrule{\kprefix[black]{cfg}{\kprefix[black]{k}{\terminal{not}B}}}
{\kprefix[black]{cfg}{\kprefix[black]{k}{\neg B}}}{}\\
&\rrule{\kprefix[black]{cfg}{\kprefix[black]{k}{\terminal{skip}\;}}}
{\kprefix[black]{cfg}{\kprefix[black]{k}{}}}{}\\
&\rrule{\kprefix[black]{cfg}{\kprefix[black]{k}{S_1;S_2}}}
{\kprefix[black]{cfg}{\kprefix[black]{k}{S_1\kra S_2}}}{}\\
&\rrule{\kprefix[black]{cfg}{\kprefix[black]{k}{\terminal{\{}S\terminal{\}}}}}
{\kprefix[black]{cfg}{\kprefix[black]{k}{S}}}{}\\
&\rrule{\kprefix[black]{cfg}{\kprefix[black]{k}{\terminal{if}\true\terminal{}S_1\terminal{else}S_2}}}
{\kprefix[black]{cfg}{\kall[black]{k}{S_1}}}{}\\
&\rrule{\kprefix[black]{cfg}{\kall[black]{k}{\terminal{if}\false\terminal{}S_1\terminal{else}S_2}}}
{\kprefix[black]{cfg}{\kall[black]{k}{S_2}}}{}\\
&\rrule{\kprefix[black]{cfg}{\kprefix[black]{k}{\terminal{while}B\terminal{do}S}}}{}{}
{}\\
&\quad{\kprefix[black]{cfg}{\kprefix[black]{k}{\terminal{if}B\terminal{}\terminal{\{}S\terminal{;}
\terminal{while}B\terminal{do}S\terminal{\}}\terminal{else}\ \terminal{skip}}}}\\
&\rrule{\kall[black]{cfg}{\kprefix[black]{k}{X}\kall[black]{env}{M}}}
{\kall[black]{cfg}{\kprefix[black]{k}{lookup(X,M)}\kall[black]{env}{M}}}{}\\
&\rrule{\kall[black]{cfg}{\kprefix[black]{k}{X\terminal{:=}I}\kall[black]{env}{M}}}
{\kall[black]{cfg}{\kprefix[black]{k}{}\kall[black]{env}{update(X,M,I)}}}{}
\end{aligned}
$
\hrule
\end{center}
\end{minipage}~\vspace{2ex}
\caption{\label{imp:sem}\K Semantics of IMP}
\end{figure}


In addition to the rules shown in Figure~\ref{imp:sem} the semantics of \IMP also includes so called {\it heating}/{\it cooling} rules, induced by the \textit{strict} attribute. We show only the case of the $\terminal{if}$ statement, which is strict in the first argument. The evaluation of this argument is achieved by executing the following rules:\\[1ex]
\centerline{
%\fontsize{9}{10}
%\selectfont
$\begin{array}{lr}
\hspace{-5ex}\!\phantom{B\kra}\!\kprefix[black]{cfg}{\kall[black]{k}{\terminal{if}\!\mathit{BE} \hspace{.5ex} S_1\terminal{else} S_2\kra C}}
\pmb{\Rightarrow}\\
\hspace{10ex}\kprefix[black]{cfg}{\kall[black]{k}{\mathit{BE}\!\kra\terminal{if} \square \hspace{.5ex} S_1\terminal{else} S_2{\kra} C}}\\
\hspace{-1ex}\!\kprefix[black]{cfg}{\kall[black]{k}{B\!\kra\terminal{if} ~\square~  S_1\terminal{else} S_2\kra C}} 
\pmb{\Rightarrow}\\
\phantom{\mathit{BE}\kra} 
\hspace{4ex}\!\kprefix[black]{cfg}{\kall[black]{k}{\terminal{if} B  S_1\terminal{else} S_2{\kra} C}}
\end{array}
$}\\[0.5ex]

Here, $BE$ ranges over \sort{BExp} $\setminus\{\false,\true\}$, $B$ ranges over the Boolean values $\{\false,\true\}$, and 
$\square$ is a special variable, destined to receive the value of $BE$ once it is computed, typically, by the other   rules in the semantics.


\section{Hoare Logic vs. Matching Logic reachability}
\label{sec:all}
\subsection{Hoare Logic}
\label{sec:hoare}
The goal of Hoare Logic is to provide a formal system for reasoning about program correctness. The axioms and the deduction rules of this system provide a method of proving statements of the form $\{\psi\}{\mathit St}\{\psi'\}$ (i.e. Hoare triples), where ${\mathit St}$ is a program statement, and $\psi$ and $\psi'$ are assertions involving program variables. 
%Hoare triples are called {\it partial correctness assertions}. They are {\it partial} because they allow statements to be undefined. 
%In Hoare logic, only partial correctness can be proven, while termination needs to be proved separately.
 Formally, a Hoare triple $\{\psi\}{\mathit St}\{\psi'\}$ is called {\it valid} (w.r.t. partial correctness) if and only if for any program state $\sigma$, which satisfies the assertion $\psi$, if the statement ${\mathit St}$ is defined in state $\sigma$ and ends up in a state $\sigma'$, then $\sigma'$ satisfies $\psi'$. We denote by $\sigma \models \psi$ the fact that $\sigma$ satisfies $\psi$ and by $\models \{\psi\}{\mathit St}\{\psi'\}$  the fact that $\{\psi\}{\mathit St}\{\psi'\}$ is valid.

%In one of his influential books~\cite{DBLP:books/ph/Dijkstra76}, Dijkstra regarded the precondition $\psi$ and the postcondition $\psi'$ as predicates on the program state, since for a given state these assertions can be either true or false. He describes a framework for specifying semantics based on `predicate transformers', which are rules for transforming predicates on states. Predicate transformer semantics are a reformulation of Floyd-Hoare Logic. Since Hoare Logic is presented as a deductive system, predicate transformer semantics (either by {\it weakest-preconditions} or by {\it strongest-postconditions}) are complete strategies to build valid deductions of Hoare logic. In other words, there is an algorithm which reduces the problem of verifying a Hoare triple to the problem of proving a first-order formula. From a technical point of view, predicate transformer semantics performs a kind of symbolic execution of statements ${\mathit St}$ into predicates: execution runs {\it backward} in the case of weakest-preconditions, or runs {\it forward} in the case of strongest-postconditions.



\begin{figure}
\centering
\begin{tabular}{c}
$\ax{HL-skip}\dfrac{}{\htriple{\psi}{\tt skip}{\psi}}$ \hspace{1cm}  $\ax{HL-block}\dfrac{\htriple{\psi}{St}{\psi'}} {\htriple{\psi}{\terminal{\{}St\terminal{\}}}{\psi'}}$\\[4ex]
$\ax{HL-assign}\dfrac{}{\htriple{\psi}{X \terminal{\tt :=} E}{(\exists x)X=E[x/X]\land \psi[x/X]}}$\\[4ex]
$\ax{HL-seq}\dfrac{\htriple{\psi_1}{St_1}{\psi_2}\quad \htriple{\psi_2}{St_2}{\psi_3}}{\htriple{\psi_1}{St_1\terminal{\tt ;}St_2}{\psi_3}}$\\[4ex]
$\ax{HL-while}\dfrac{\htriple{\psi\land BE}{St}{\psi}}{\htriple{\psi}{\terminal{while\,(}BE\terminal{)\,do}St}{\psi\land\neg BE}}$\\[4ex]
$\ax{HL-if}\dfrac{\htriple{\psi\land BE}{St_1}{\psi'} \hspace{2ex} \htriple{\psi\land \neg BE}{St_2}{\psi'}}{{\htriple{\psi}{\terminal{if\,(}BE\terminal{)}St_1\terminal{else}St_2}{\psi'}}}$\\[4ex]
$\ax{HL-cseq}\dfrac{\psi\rightarrow\psi_1\quad\htriple{\psi_1}{St}{\psi'_1}\quad\psi'_1\rightarrow\psi'} {\htriple{\psi}{St}{\psi'}}$\\[2ex]
\end{tabular}
\caption{\label{imp:h}Floyd-Hoare proof system for \IMP}
\end{figure}


The Hoare Logic deduction system for \IMP is shown in Figure~\ref{imp:h}. It contains a set of deduction rules which correspond to each construct of the language. The deduction system can be used only to prove Hoare triples w.r.t partial correctness.
%For every \IMP statement there is a corresponding deduction rule. The deduction rules for the empty statement \ax{HL-skip} and for blocks of statements \ax{HL-block} assert that after the execution of these instructions, the program state is not changed. The \ax{HL-assign} axiom states that after the assignment any predicate holds for the variable that was previously true for the right-hand side of the assignment. This is equivalent to saying that to find the precondition, first take the post-condition and replace all occurrences of the left-hand side of the assignment with the right-hand side of the assignment. The composition rule \ax{HL-seq} applies to sequentially executed programs ${\mathit St_1}$ and ${\mathit St_2}$, where ${\mathit St_1}$ executes prior to ${\mathit St_2}$. In this case, the postcondition of ${\mathit St_1}$ is the precondition of ${\mathit St_2}$, $\psi_2$ being also called {\it midcondition}. The rule corresponding to the \mytt{while} loop (\ax{HL-while}) uses a loop invariant $\psi$, which holds before and after the loop body ${\mathit St}$ is executed. After the execution, when the loop condition ${\mathit BE}$ becomes false, the postcondition is the conjunction of the invariant $\psi$ and $\neg{\mathit BE}$. The conditional rule \ax{HL-if} states that a postcondition $\psi'$ common to both branches ({\it then}, {\it else}) is also a postcondition of the whole \mytt{if} statement. In the {\it then} and the {\it else} branches, the unnegated and negated condition  can be added to the precondition, respectively. The rule for consequence \ax{HL-cseq} is a bit more general, and allows to strengthen the precondition and/or to weaken the postcondition.




\subsection{Matching Logic Reachability}
\vspace{1ex}
\label{sec:rl}

%\begin{figure}[t]
%\begin{align*}
%\ax{Axiom}~  &\dfrac{(\varphi \Rightarrow \varphi') \in \S}{\S  \vdash_\C \varphi \Rightarrow \varphi'}
%\quad \quad \ax{Reflexivity}~ \dfrac{\cdot} {\S \vdash \varphi \Rightarrow \varphi}\\[1ex]  
%\ax{Transitivity}~          
%& \dfrac{\S \vdash_\C \varphi \Rightarrow^{+} \varphi'' \quad (\S \cup \C) \vdash \varphi'' \Rightarrow \varphi'}{\S \vdash_\C \varphi \Rightarrow \varphi'}\\[1ex]
%\ax{LogicFraming}~          
%& \dfrac{\S \vdash \varphi \Rightarrow \varphi' \quad \mathit{\psi \ patternless \ FOL \ formula}}{\S \vdash \varphi \land \psi\Rightarrow \varphi' \land \psi}\\[1ex]
%\ax{Consequence}~ 
%&
%\dfrac{\models \varphi_1 \to \varphi'_1 \quad \S \vdash_\C \varphi'_1 \Rightarrow \varphi'_2 \quad \models \varphi'_2 \to \varphi_2}
%          {\S \vdash_\C \varphi_1 \Rightarrow \varphi_2}\\[1ex]
%\ax{CaseAnalysis}~          
%& \dfrac{\S \vdash_\C \varphi_1 \Rightarrow \varphi \quad \S \vdash_\C  \varphi_2 \Rightarrow \varphi}{\S \vdash_\C (\varphi_1 \vee \varphi_2) \Rightarrow \varphi}\\[1ex]
%\ax{Abstraction}~  
%& \dfrac{\S \vdash_\C \varphi \Rightarrow \varphi' \quad X \cap \mathit{FreeVars}(\varphi') = \emptyset}{\S \vdash_\C (\exists  X.\,\varphi) \Rightarrow \varphi' }\\[1ex]         
%\ax{Circularity}~          
%& \dfrac{\S \vdash_{\C \cup\{ \varphi \Rightarrow \varphi' \}}\varphi \Rightarrow \varphi'}{\S \vdash_C\varphi \Rightarrow \varphi'}
%\end{align*}
%\caption{\label{fig:origrl} Language-independent deductive system for Matching Logic reachability.}
%\end{figure}


In MLR~\cite{rosu-stefanescu-2012-fm} program configurations are specified using {\it patterns} $\varphi$, which are first-order logic (FOL) formulas that allow configuration terms with variables as predicates. More precisely, patterns are expressions of the form $\pattern{\pi}{b}$, where $\pi$ defines a set of (concrete) configurations, and the condition $b$ gives additional constraints these configurations must satisfy. We write $(\gamma,\rho)\models\pattern{\pi}{b}$ whenever the variable assignment $\rho$ satisfies $b$ and $\rho(\pi)=\gamma$ ($\gamma$ is a concrete configuration).

Reachability rules specify operational transitions or program properties.  A reachability rule is a pair $\varphi \Rightarrow \varphi'$, where $\varphi$ and $\varphi'$ are patterns (which can have free variables). Semantic validity in MLR captures the same intuition of partial correctness as Hoare logic, but in more general terms of reachability: $\models \varphi \Rightarrow \varphi'$ w.r.t. partial correctness iff for each $(\gamma, \rho)$  with $(\gamma, \rho)\models \varphi$ and $\gamma$ terminating, there is $\gamma'$ s.t. $(\gamma', \rho)\models \varphi'$.


%Matching Logic reachability provides a language independent proof system (see Figure~\ref{fig:origrl}) that takes a set of reachability rules (operational semantics) as axioms and derives new reachability rules (program properties). It derives sequents of the form $\S \vdash_\C \varphi \Rightarrow \varphi'$, where $\S$ and $\C$ are sets of reachability rules. Initially, $\S$ contains the operational semantics of the target language, given as a set of (one-step) reachability rules, and $\C$, the set of circularities, is empty. A sequent $\S \vdash \varphi \Rightarrow \varphi'$ denotes an empty set of circularities. The intuition for a sequent $\S \vdash_\C \varphi \Rightarrow \varphi'$ is that the reachability rule $\varphi \Rightarrow \varphi'$ holds under the hypotheses $\S$ and $\C$, provided that the first step is always one from $\S$ whenever $\C$ is non-empty. In other words, the existence of a (non-empty) $\C$ in a sequent $\S \vdash_\C \varphi \Rightarrow \varphi'$ requires its derivation to start with a trusted step, that is, a step corresponding to a trusted rule in $\S$, and then to continue unrestricted using steps from both $\S$ and $\C$.
%An example which has been proved correct using the Matching Logic reachability proof system is \mytt{SUM}~\cite{rosu-stefanescu-2012-fm}.
If \mytt{SUM} is a macro for the \IMP program "\mytt{S = 0; i = 1; while (i <= n) \{ S = S + i;  i = i + 1;\}}", then  the pattern $(\exists s) (\kall[black]{cfg}{\kall[black]{k}{\mathtt{SUM}}, \kall[black]{env}{\mathtt{S} \mapsto s, \mathtt{n} \mapsto n, \mathtt{i} \mapsto i}}\, \land n \geq 0)$
is matched by the configurations containing code \mytt{SUM} and state mapping program variables \mytt{S}, \mytt{n}, \mytt{i} into integers $s$, $n$, $i$ with $n$ positive. Note that, unlike in Hoare Logic, Matching Logic makes a clear distinction between program and logical variables, and between program operators. The same applies to language
arithmetic constructs versus mathematical domain operations(e.g. {\bf \mytt{+}} in the language vs. $+_{Int}$ in the mathematical domain). The following reachability rule:~\vspace{-1ex}
\begin{center}
$(\exists s) (\kall[black]{cfg}{\kall[black]{k}{\mathtt{SUM}}\kall[black]{env}{\mathtt{S} \mapsto s, \mathtt{n} \mapsto n, \mathtt{i} \mapsto i}}\, \land n \geq 0) \Rightarrow$~\\
$\kall[black]{cfg}{\kall[black]{k}{\mathtt{skip}}\kall[black]{env}{\mathtt{S} \mapsto n *_{Int} (n +_{Int} 1) /_{Int} \text{ } 2, \mathtt{n} \mapsto n, \mathtt{i} \mapsto n}}$~\vspace{-1ex}
\end{center}
specifies the property of the \mytt{SUM} program. Unlike Hoare triples, reachability rules can specify properties about intermediate states of programs, not only for final states. So, Hoare triples are particular reachability rules, where all the patterns from the right hand side of the rule contain the empty $\kall[black]{k}{.}$ cell.  



\subsection{Transforming Hoare triples into reachability rules}

\label{sec:transform}
For the \IMP language, a Hoare triple $\htriple{\psi}{St}{\psi'}$ can be encoded as the following reachability rule:\vspace*{-1ex}

\begin{table}[H]
\captionsetup{labelformat=empty}
\begin{center}
%\begin{equation}
\fontsize{10.5}{12}
\selectfont
\begin{tabular}{l r}
$(\exists {X})\kall[black]{cfg}{\kall[black]{k}{St}\kall[black]{env}{\sigma_{X}}}\land\psi_{X,Y}\Rightarrow$
& \multirow{2}{*}{(I)} \\
\hspace{2cm}$(\exists{X})\kall[black]{cfg}{\kall[black]{k}{\kdot}\kall[black]{env}{\sigma_{X}}}\land\psi'_{X,Y}$ &\\
\end{tabular}~\vspace*{-4ex}
\caption{\label{transf}}
%\end{equation}
\end{center}
\end{table}

\vspace*{-3ex}\noindent$X$ and $Y$ are two disjoint sets of variables corresponding to two sets \mytt{X}, \mytt{Y}, which contain the program variables which appear in ${\mathit St}$, and the additional variables that appear in $\psi$ and $\psi'$ but not in \mytt{X}, respectively. We use $X$ and $Y$ instead of \mytt{X} and \mytt{Y} because Matching Logic distinguishes between program and logical variables. This restriction does not limit Hoare Logic in any way, because we can always choose \mytt{X} as being the set of all program variables about which we want to reason and \mytt{Y} the rest of variables occurring anywhere in the state or the specification, but different from \mytt{X}.
$\sigma_X$ is the state mapping each \mytt{x \in X} to its corresponding $x\in X$. Formulas $\psi_{X,Y}$ and $\psi'_{X,Y}$ are $\psi$ and respectively $\psi'$ with \mytt{x \in X} and \mytt{y \in Y} replaced by its corresponding $x\in X$ and $y\in Y$, and each expression construct (e.g. \mytt{+}) replaced by its mathematical correspondent (e.g. $+_{Int}$).

A Hoare triple is semantically valid $\models \{\psi\}St\{\psi'\}$ iff  $\models (\exists {X})\kall[black]{cfg}{\kall[black]{k}{St}\kall[black]{env}{\sigma_{X}}}\land\psi_{X,Y}\Rightarrow (\exists{X})\kall[black]{cfg}{\kall[black]{k}{\kdot}\kall[black]{env}{\sigma_{X}}}\land\psi'_{X,Y}$. Therefore, we can prove Hoare triples by proving reachability rules.
It has been shown in ~\cite{rosu-stefanescu-2012-fm} that for the IMP language, any Hoare logic proof derivation
of a Hoare triple $\htriple{\psi}{St}{\psi'}$ yields a matching logic reachability proof derivation of
the corresponding reachability rule.  

\begin{figure}[t]
\fontsize{9}{11}
\selectfont
\begin{tabular}{c}
$\ax{HL'-skip}\dfrac{}
{(\exists {X})\kall[black]{cfg}{\kall[black]{k}{\terminal{skip}}\kall[black]{env}{\sigma_{X}}}\land\psi_{X,Y}\Rightarrow}$\\
$(\exists{X})\kall[black]{cfg}{\kall[black]{k}{\kdot}\kall[black]{env}{\sigma_{X}}}\land\psi_{X,Y}$\\[3ex]

$\ax{HL'-assign}\dfrac{}
        {(\exists {X})\kall[black]{cfg}{\kall[black]{k}{{\tt X}\terminal{:=}E}\kall[black]{env}{\sigma_{X}}}\land\psi_{X,Y}\Rightarrow}$\\
$(\exists{X})\kall[black]{cfg}{\kall[black]{k}{\kdot}\kall[black]{env}{\sigma_{X}}}\land ((\exists x)(x =E[x/X]\land\psi_{X,Y}[x/X]))$\\[3ex]
$\ax{HL'-seq}\dfrac{
\begin{aligned}
(\exists {X})\kall[black]{cfg}{\kall[black]{k}{St_1}\kall[black]{env}{\sigma_{X}}}\land\psi^1_{X,Y}\Rightarrow\\
(\exists{X})\kall[black]{cfg}{\kall[black]{k}{\kdot}\kall[black]{env}{\sigma_{X}}}\land\psi^2_{X,Y}\\
(\exists {X})\kall[black]{cfg}{\kall[black]{k}{St_2}\kall[black]{env}{\sigma_{X}}}\land\psi^2_{X,Y}\Rightarrow\\
(\exists{X})\kall[black]{cfg}{\kall[black]{k}{\kdot}\kall[black]{env}{\sigma_{X}}}\land\psi^3_{X,Y}
\end{aligned}}
       {(\exists {X})\kall[black]{cfg}{\kall[black]{k}{St_1 St_2}\kall[black]{env}{\sigma_{X}}}\land\psi^1_{X,Y}\Rightarrow}$\\
${(\exists{X})\kall[black]{cfg}{\kall[black]{k}{\kdot}\kall[black]{env}{\sigma_{X}}}\land\psi^3_{X,Y}}$\\[3ex]
$(\exists {X})\kall[black]{cfg}{\kall[black]{k}{St}\kall[black]{env}{\sigma_{X}}}\land\psi_{X,Y}\Rightarrow$\\
$\ax{HL'-block}\dfrac{(\exists{X})\kall[black]{cfg}{\kall[black]{k}{\kdot}\kall[black]{env}{\sigma_{X}}}\land\psi'_{X,Y}}
        {(\exists {X})\kall[black]{cfg}{\kall[black]{k}{\terminal{\{}St\terminal{\}}}\kall[black]{env}{\sigma_{X}}}\land\psi_{X,Y}\Rightarrow}$\\
${(\exists{X})\kall[black]{cfg}{\kall[black]{k}{\kdot}\kall[black]{env}{\sigma_{X}}}\land\psi'_{X,Y}}$\\[3ex]
$(\exists {X})\kall[black]{cfg}{\kall[black]{k}{St}\kall[black]{env}{\sigma_{X}}}\land\psi_{X,Y}\land BE\Rightarrow$\\
$\ax{HL'-while}\dfrac{(\exists{X})\kall[black]{cfg}{\kall[black]{k}{\kdot}\kall[black]{env}{\sigma_{X}}}\land\psi_{X,Y}}
        {(\exists {X})\kall[black]{cfg}{\kall[black]{k}{\terminal{while\,(}BE\terminal{)\,do}St}\kall[black]{env}{\sigma_{X}}}\land\psi_{X,Y}\Rightarrow}$\\
${(\exists{X})\kall[black]{cfg}{\kall[black]{k}{\kdot}\kall[black]{env}{\sigma_{X}}}\land\psi_{X,Y}\land\neg BE}$\\[3ex]
$\ax{HL'-if}\dfrac{\begin{aligned}
(\exists {X})\kall[black]{cfg}{\kall[black]{k}{St_1}\kall[black]{env}{\sigma_{X}}}\land\psi_{X,Y}\land BE\Rightarrow\\
(\exists{X})\kall[black]{cfg}{\kall[black]{k}{\kdot}\kall[black]{env}{\sigma_{X}}}\land\psi'_{X,Y}\\
(\exists {X})\kall[black]{cfg}{\kall[black]{k}{St_2}\kall[black]{env}{\sigma_{X}}}\land\psi_{X,Y}\land\neg BE\Rightarrow\\
(\exists{X})\kall[black]{cfg}{\kall[black]{k}{\kdot}\kall[black]{env}{\sigma_{X}}}\land\psi'_{X,Y}
\end{aligned}}
        {(\exists {X})\kall[black]{cfg}{\kall[black]{k}{\terminal{if\,(}BE\terminal{)}St_1\terminal{else}St_2}\kall[black]{env}{\sigma_{X}}}\land\psi_{X,Y}\Rightarrow}$\\
${(\exists{X})\kall[black]{cfg}{\kall[black]{k}{\kdot}\kall[black]{env}{\sigma_{X}}}\land\psi'_{X,Y}}$\\[3ex]
$\ax{HL'-cseq}\dfrac{\psi\Rightarrow\psi^{1}\quad
\begin{aligned}(\exists {X})\kall[black]{cfg}{\kall[black]{k}{St}\kall[black]{env}{\sigma_{X}}}\land\psi^{1}_{X,Y}\Rightarrow\\
(\exists{X})\kall[black]{cfg}{\kall[black]{k}{\kdot}\kall[black]{env}{\sigma_{X}}}\land{\psi}^{2}_{X,Y}
\end{aligned}
\quad{\psi}^{2}\Rightarrow\psi'}
        {(\exists {X})\kall[black]{cfg}{\kall[black]{k}{St}\kall[black]{env}{\sigma_{X}}}\land\psi_{X,Y}\Rightarrow}$\\
$\hspace{5ex}{(\exists{X})\kall[black]{cfg}{\kall[black]{k}{\kdot}\kall[black]{env}{\sigma_{X}}}\land\psi'_{X,Y}}$
\end{tabular}
\caption{\label{imp:ml}\ax{HL'-IMP}: the equivalent Floyd-Hoare proof system given using Matching Logic reachability rules. Each Hoare triple from the Floyd-Hoare deduction system~\ref{imp:h} has been transformed into an equivalent reachability rule using ~\ref{transf}.}
\end{figure}

We applied the transformation~\ref{transf} to the Floyd-Hoare proof system for \IMP (Figure~\ref{imp:h}) and we obtained the equivalent Floyd-Hoare proof system given using Matching Logic reachability rules (\ax{HL'-IMP}) shown in Figure~\ref{imp:ml}.

%\tbd{ML este "missleading". Propun sa utilizezi HL' in loc; de fapt este tot Hoare logic, dar cu alta sintaxa. ML este deja adjudecat pentru alta logica.}

\section{Symbolic execution and reachability rules}
\label{sec:proof}

In~\cite{arusoaie:hal-00766220}, we proposed a language-independent approach for languages, endowed with a formal operational semantics based on term rewriting. Starting from the definition of a language $\cal L$, a new definition ${\cal L}^{\it sym}$ is automatically generated, which has the same syntax, but whose semantics extends ${\cal L}$'s data domains with symbolic values and adapts the semantical rules of $\cal L$ to deal with the new domains. Then, the symbolic execution of ${\cal L}$ programs is the concrete execution of the corresponding ${\cal L}^{\it sym}$ programs, i.e., the application of the rewrite rules in the semantics of ${\cal L}^{\it sym}$. 
Our approach, is based on three mechanical steps which are applied to the operational semantics $\S$ of the language ${\cal L}$:
\begin{enumerate}
\label{steps}
\item {\it Linearising rules}. A nonlinear rule (i.e. it contains variables that occur twice in the left hand side) is turned into an equivalent linear one, by renaming the variables occurring several times and adding equalities between the renamed variables and the original ones to the rule's condition.
\item {\it Replacing Data Subterms by Variables}. This step replaces any constant (data subterm) $c$ with a variable $X$ which has the same sort as $c$, and appends the equality $X=c$ to the side condition of the rule.
\item {\it Adding Formulas to Configurations and Rules}. This step consists in adding a new cell to the configuration for holding the path condition during execution. Each rewrite rule $l \land b \Ra r $ is transformed into $\rrule{\langle l,\psi\rangle}{\langle r,\psi \land b \rangle}{}$. This means that when a symbolic transition is performed on a symbolic configuration the current path condition is enriched with the rule's condition. The configuration is enriched with the path condition cell $\kall[black]{cond}{}$ and becomes: $\kall[black]{cfg}{\kall[black]{k}{\sort{Code}}\kall[black]{env}{\sort{Map}_{\mathit{Id},\mathit{Int}}}\kall[black]{cond}{true}}$
%$
%\begin{array}{ll}
%\sort{Cfg}&::=\kall[black]{cfg}{\kall[black]{k}{\sort{Code}}\kall[black]{env}{\sort{Map}_{\mathit{Id},\mathit{Int}}}\kall[black]{cond}{true}}
%\end{array}
%$
\end{enumerate}

\noindent Our symbolic execution has the natural properties of {\it coverage}, meaning that to each concrete execution there is a feasible symbolic one on the same path of instructions, and {\it precision}, meaning that each feasible symbolic execution has a concrete execution on the same path. Moreover, we can use the framework to execute patterns $\varphi=\pi\land\psi$ by setting $\kall[black]{cfg}{\kall[black]{}{\pi} \kall[black]{cond}{\psi}}$ to be the initial configuration.

In this paper, we use symbolic execution to find all possible executions of a pattern $\varphi$, that is, all patterns $\varphi'$ that are reachable from $\varphi$.
%If $\varphi$ is an \IMP pattern $\kall[black]{cfg}{\kall[black]{k}{St}\kall[black]{env}{\sigma_{X}}}\land\psi_{X,Y}$, where $\sigma_X$ is a map binding program variables \mytt{X} to logical variables $X$, and $\psi_{X,Y}$ a formula which constrains $X$, then symbolic execution of $\varphi$ executes ${\mathit St}$ and appends new constraints to $\psi_{X,Y}$
%, without changing $\sigma_X$. 
If $\varphi'$ contains an empty $\kall[black]{k}{\kdot}$ cell then the execution completed successfully. In the following, we use the symbol $\Ra\!\!\!^*$ to denote zero, one, or more applications of rewrite rules from the symbolic semantics. We prove that a successful symbolic execution $\varphi \Ra\!\!\!^* \varphi'$ yields a reachability rule $\varphi \Rightarrow \varphi'$ which can be proved using \ax{HL'-IMP}.

%In some sense, this approach is the same as the one described in ~\cite{Gordon10}, because we collect all the constraints performing {\it forward} execution.
%Obviously, we are only interested in {\it complete} executions:

\begin{definition}[irreductible pattern]
Let $\varphi$ and $\varphi'$ be patterns. $\varphi$ is \emph{irreducible} iff there is no $\varphi'$ such that $\varphi\Ra\varphi'$.
\end{definition}

%\tbd{Imi pare rau, dar definitiile de mai jos tot nu e corecta. Cred ca trebuie sa te referi la toate executiile complete, care nu mai pot fi continuate. O posibila varianta corecta (scriu varianta lunga ca sa se ineleaga):\\
%$\varphi$ is \emph{irreducible} iff there is no $\varphi'$ such that $\varphi\Ra\varphi'$.\\
%A \emph{complete execution} is an execution $\varphi\mathrel{{\Ra}^*}\varphi'$ such that $\varphi'$ is irreducible. We denote a complete execution by $\varphi\mathrel{{\Ra}^!}\varphi'$. \\
%A complete execution $\varphi\mathrel{{\Ra}^!}\varphi'$ is \emph{successfull} if $\varphi'$ contains the empty $\kall[black]{k}{\kdot}$ cell.\\
%$\varphi\!\!\downarrow$ iff all complete execution starting from $\varphi$ are successful.\\
%$RL(\varphi) = \{\varphi\Rightarrow\varphi' \mid \varphi\mathrel{{\Ra}^!}\varphi'\}$.
%}


\begin{definition}[complete and successful execution]
\label{def:complete}
A \emph{complete execution} is an execution $\varphi\mathrel{{\Ra}\!^*}\varphi'$ such that $\varphi'$ is irreducible.
A complete execution is \emph{successful}, and we write $\varphi\mathrel{{\Ra}^!}\varphi'$, if $\varphi'$ contains an empty $\kall[black]{k}{\kdot}$ cell. We say that $\varphi\!\!\downarrow$ holds iff all complete executions starting from $\varphi$ are successful.
\end{definition}



%\tbd{De explicat $\Ra\!\!\!\!\!\!\!^*$ inainte de prima utilizare.}
\noindent Definition~\ref{def:complete} says that all the symbolic executions starting with $\kall[black]{cfg}{\kall[black]{k}{St}\kall[black]{env}{\sigma_{X}}}\land\psi_{X,Y}$ are successful if and only if ${\mathit St}$ is consumed during the execution.
Next, we define the set of reachability rules derived from $\varphi$ as follows:

\begin{definition}
Let $\varphi$ be a pattern. We define the set $RL(\varphi)$ of reachability rules as follows: $$RL(\varphi) = \{\varphi\Rightarrow\varphi' \mid \varphi\Ra\!\!^!\varphi'\}$$
\end{definition}

\noindent $RL(\varphi)$ contains all the reachability rules $\varphi \Rightarrow \varphi'$, s.t. $\varphi'$ is reachable from $\varphi$ and contains the empty $\kall[black]{k}{\kdot}$ cell. Theorem~\ref{th} shows that any $\varphi \Rightarrow \varphi' \in RL(\varphi)$ can be derived using \ax{HL'-IMP}.

\begin{theorem}
\label{th}
Let $\varphi \eqbydef \kall[black]{cfg}{\kall[black]{k}{St}\kall[black]{env}{\sigma_{X}}}\land\psi_{X,Y}$ be a pattern.
Then:
\begin{enumerate}
\item Any reachability rule $\varphi \Rightarrow \varphi' \in RL(\varphi)$ can be proved using $\mathrm{\ax{HL'-IMP}}$.
\item Let $\varphi\Rightarrow\varphi'$ be a reachability rule such that $\varphi\!\!\downarrow$. If for each $\varphi''\in RL(\varphi)$ we have $\varphi''\rightarrow\varphi'$ then $\varphi \Rightarrow \varphi' $ can be proved using \ax{HL'-IMP}.
\end{enumerate}
%\tbd{Cred ca la 1) nu ai nevoie de  $\varphi\!\!\downarrow$.\\
%Cu noile notatii, cred ca 2) ar trebui sa sune asa:\\
%Let $\varphi\Rightarrow\varphi'$ be a reachability rule such that $\varphi\!\!\downarrow$. If for each $\varphi''\in RL(\varphi)$ we have $\varphi''\rightarrow\varphi'$ then $\varphi \Rightarrow \varphi' $ can be proved using \ax{HL'-IMP}.
%}
\end{theorem}

\begin{proof}
We proceed by structural induction on the formal proof of $\kall[black]{cfg}{\kall[black]{k}{St}\kall[black]{env}{\sigma_{X}}}\land\psi_{X,Y} \Rightarrow \kall[black]{cfg}{\kall[black]{k}{.}\kall[black]{env}{\sigma'_{X'}}}\land\psi'_{X',Y'}$ derived using \ax{HL'-IMP}:

\begin{itemize}
\item ${\mathit St}$ is \mytt{skip}. In this case, $\kall[black]{cfg}{\kall[black]{k}{\terminal{skip}}\kall[black]{env}{\sigma_{X}}}\land\psi_{X,Y} \Rightarrow \kall[black]{cfg}{\kall[black]{k}{.}\kall[black]{env}{\sigma_{X}}}\land\psi_{X,Y}$ can be derived applying \ax{HL'-skip}, because the set $X$ does not change.
\item ${\mathit St}$ is an assignment. In this case we have to derive $\kall[black]{cfg}{\kall[black]{k}{X\terminal{:=}E}\kall[black]{env}{\sigma_{X}}}\land\psi_{X,Y} \Rightarrow \kall[black]{cfg}{\kall[black]{k}{.}\kall[black]{env}{\sigma'_{X'}}}\land\psi'_{X',Y'}$ ($\spadesuit$). After the assignment statement $X \terminal{:=} E $ is executed, the logical variable $X$, which corresponds to program variable \mytt{X}, is constrained to be equal to $E$. Therefore, $\psi'_{X',Y'}$ becomes $\psi_{X,Y} \land X = E$, which is equivalent with $\psi'_{X',Y'} = ((\exists x)(x =E[x/X]\land\psi_{X,Y}[x/X]))$. If we apply \ax{HL'-assign} we can deduce ($\spadesuit$).
\item ${\mathit St}$ is an \mytt{if} statement.  We have to derive $\kall[black]{cfg}{\kall[black]{k}{\terminal{if\,(}BE\terminal{)}St_1\terminal{else}St_2}\kall[black]{env}{\sigma_{X}}}\land\psi_{X,Y}\Rightarrow\kall[black]{cfg}{\kall[black]{k}{\kdot}\kall[black]{env}{\sigma_{X}}}\land\psi'_{X,Y}$ ($\clubsuit$). But, when executing symbolically the \mytt{if} statement, $St_1$ and $St_2$ execute only if $\psi_{X,Y} \land BE$, and $\psi_{X,Y} \land \neg BE$ hold, respectively. Thus, from the induction hypothesis we have $\kall[black]{cfg}{\kall[black]{k}{St_1}\kall[black]{env}{\sigma_{X}}}\land\psi_{X,Y}\land BE\Rightarrow
\kall[black]{cfg}{\kall[black]{k}{\kdot}\kall[black]{env}{\sigma_{X}}}\land\psi'_{X,Y}$ and 
$\kall[black]{cfg}{\kall[black]{k}{St_2}\kall[black]{env}{\sigma_{X}}}\land\psi_{X,Y}\land\neg BE\Rightarrow
\kall[black]{cfg}{\kall[black]{k}{\kdot}\kall[black]{env}{\sigma_{X}}}\land\psi'_{X,Y}$. Therefore, ($\clubsuit$) can be derived applying \ax{HL'-if}.\vspace{.5ex}
\end{itemize}
The proof derivations for the remaining statements can be obtained applying the inductive hypothesis in the same manner as we did for the \mytt{if} statement.~\vspace{1ex}
\end{proof}

\noindent Theorem~\ref{th} states that symbolic execution actually ``proves'' a set of reachability rules $\varphi \Rightarrow \varphi'$. Thus, given a Hoare triple, we can transform it into a reachability rule and then prove it using symbolic execution.

\section{Implementing Hoare Logic using Symbolic Execution}
\label{sec:methodology}

In this section we present a methodology which transforms the \K specification of a programming language such that it can be used for verification. 
It captures both the transformation of Hoare triples and the verification of its corresponding reachability rules.
Users have to add syntax and semantics to the existing \K definition such that programs annotated with precondition, postcondition, and invariants for loops can be parsed and transformed into reachability rules. If $\varphi \Rightarrow \varphi'$ is a reachability rule corresponding to a Hoare triple, then the symbolic execution of $\varphi$ proves a set of reachability rules $RL(\varphi)$(Theorem ~\ref{th}), which is then used to prove $\varphi \Rightarrow \varphi'$.\vspace{1ex}

The methodology consists in adding the following features to the \K semantics of the language:

\begin{enumerate}
\item Add syntax and semantics for Hoare-like annotations.
\item Define \mytt{assume} and \mytt{implies} operations for checking reachability formulas.
\end{enumerate}

\noindent Note that these new features do not change the original semantics of the language, but they affect the syntax of programs by adding support for Hoare annotations.\vspace{1ex}

The first feature which has to be added to the \K semantics of the target language is related to the transformation of Hoare triples into reachability rules. First, we need to add syntax for Hoare-like annotations (i.e. preconditions, postconditions, and invariants). 
At the implementation level, we create a sort $\sort{Assert}$ for assertions, which usually extends the Boolean expressions of the language. In the case of \IMP, $\sort{Assert}$ includes the sort $\sort{BExp}$. Users can create their own syntax and semantics for assertions but they have to allow program variables in their syntax.
Once we have a sort for assertions we can give syntax for the preconditions, postconditions, and invariants.
For \IMP, we assume that Hoare triples have the following syntax:\vspace{-1ex}
\[ 
\fontsize{10}{11}
\selectfont
{\terminal{pre:}}\sort{Assert} {\terminal{post:}}\sort{Assert}\text{ }\sort{Stmt}~\vspace{-1ex}
\] 

\noindent The syntax of the annotated ${\terminal{while}}$ loop is:~\vspace{-1ex}
\[
\fontsize{10}{11}
\selectfont
{\terminal{while}} \sort{BExp} {\terminal{inv:}} \sort{Assert}\text{ }\sort{Stmt}~\vspace{-1ex}
\]


\noindent According to transformation~\ref{transf}, the precondition and the program become parts of the left hand side of the corresponding reachability rule. The right hand side of the reachability rule contains the postcondition, and an empty $\kall[black]{k}{\kdot}$ cell. The semantics of a Hoare triple can be given using the additional constructs \mytt{assume} and \mytt{implies} (defined later), as follows:\vspace{-2ex}

\[
%\ax{HT}:\\
\fontsize{9}{11}
\selectfont
%\hspace{-1ex}
\kall[black]{k}{
\reduce{\terminal{pre:}\psi\terminal{post:}\psi'\text{ }St}
{\terminal{assume}(\kall[black]{k}{St}\kall[black]{env}{\sigma}\kall[black]{cond}{\psi})\kra \terminal{implies}(\kall[black]{k}{\kdot}\kall[black]{env}{\sigma'}\kall[black]{cond}{\psi'})}}
%\kall[black]{env}{\AnyVar}
%\kall[black]{cond}{\AnyVar}
\]
\noindent The rewrite rule above transforms a Hoare triple into a reachability rule. Note that, the transformation~\ref{transf} quantifies existentially the logical variables corresponding to the program variables. Therefore, $\sigma$ and $\sigma'$ assign program variables with fresh symbolic values. Note that we did not mentioned the $\kall[black]{cfg}{}$ cell because in only wraps the other cells and has no semantical meaning in this case.



The operational semantics of the \mytt{while} loop with invariants, is given by the following two rewrite rules:
\[
\fontsize{9}{11}
\selectfont
\hspace{-1ex}
\kall[black]{k}{\reduce{\mathtt{while}({\it B}){\terminal{inv:}}\psi\;St\kra K}
{{\terminal{assume}}(\kall[black]{k}{St}\kall[black]{env}{\sigma}\kall[black]{cond}{B \land \psi})\!\kra\!\!\!{\terminal{implies}}(\kall[black]{k}{\kdot}\kall[black]{env}{\sigma'}\kall[black]{cond}{\psi})
}}
\]
\[
\fontsize{9}{11}
\selectfont
\hspace{-1.5ex}
\kall[black]{k}{\reduce{\mathtt{while}({\it B}){\terminal{inv:}}\psi\;St\kra K}{
{\terminal{implies}}(\kall[black]{k}{\kdot}\kall[black]{env}{\sigma'}\kall[black]{cond}{\psi})\!\kra\!\!\!
{\terminal{assume}}(\kall[black]{k}{K}\kall[black]{env}{\sigma}\kall[black]{cond}{\neg B \land \psi})}}
\]

\noindent
The above two rules breaks the annotated \mytt{while} statement in two reachability formulas: one corresponding the body of the loop $\kall[black]{cfg}{\kall[black]{k}{St}\kall[black]{env}{\sigma}}\land (B \land \psi) \Rightarrow \kall[black]{cfg}{\kall[black]{k}{\kdot}\kall[black]{env}{\sigma}} \land \psi'$,  and  another corresponding to the code outside the loop $\kall[black]{cfg}{\kall[black]{k}{K}\kall[black]{env}{\sigma}}\land (\neg B \land \psi) \Rightarrow \kall[black]{cfg}{\kall[black]{k}{\kdot}\kall[black]{env}{\sigma}} \land \psi'$.~\vspace{1ex}




Operations \mytt{assume} and \mytt{implies} are meant to verify reachability formulas. The \mytt{assume(\varphi)} construct, prepares the pattern given as argument, $\varphi$ in this case, for symbolic execution. In the case of \IMP, the semantics of \mytt{assume} is the following:\vspace{1ex}

\noindent\[
\fontsize{9}{11}
\selectfont
\kprefix[black]{k}{\reduce{\terminal{assume}(\kall[black]{cfg}{\kall[black]{k}{St}\kall[black]{env}{E}\kall[black]{cond}{\phi})}}{St}}
\kall[black]{env}{\reduce{\AnyVar}{E}}\kall[black]{cond}{\reduce{\AnyVar}{\phi}}\vspace{-1ex}
\]

\noindent The rewrite rule above fills the current symbolic configuration with the contents of the given pattern.
The symbolic semantics applies on $\varphi$ and produces a set of new configurations. If all these configuration contain the empty $\kall[black]{k}{\kdot}$ cell, then we can derive a valid set of reachability rules $RL(\varphi)$(Theorem~\ref{th}).

The \mytt{implies(\varphi')} operation checks if the current symbolic configuration, which contains a pattern $\varphi''$, implies the pattern given as argument $\varphi'$. If $\varphi\!\!\downarrow$ then $\varphi \Rightarrow \varphi'$ holds if for all $\varphi \Rightarrow \varphi'' \in RL(\varphi)$ the reachability rule $\varphi'' \Rightarrow \varphi'$ holds. In order to reduce the verification of $\varphi'' \Rightarrow \varphi'$ to an expression which can be solved using the Z3 SMT solver, we make the following assumption:%~\vspace{1ex}
\begin{assumption}
\label{asp}
Let $\varphi=\pi \land \phi$ be a pattern. Then there exists $\pi_0$, such that $(\forall \pi)(\exists \sigma)(\pi =\sigma(\pi_0))$. Moreover, for all $\varphi$ we have $\varphi = \pi_0 \land(\phi \land \bigwedge_\sigma)$, where by $\bigwedge_\sigma$ we denote the conjunction $\bigwedge_{{\mathit x} \in X}{{\mathit x} = \sigma({\mathit x})}$.
\end{assumption}

\noindent The assumption above says that, inside a pattern $\varphi=\pi\land\phi$, any configuration $\pi$ can be replaced by a more {\it general} configuration $\pi_0$ constrained by $\bigwedge_\sigma$. Therefore, $\varphi'' \Rightarrow \varphi'$ can be written as $\pi''_0 \land (\phi'' \land \bigwedge_{\sigma''}) \Rightarrow \pi'_0 \land (\phi' \land \bigwedge_{\sigma'})$. Since $\varphi\!\!\downarrow$, configuration $\pi''_0$ contains the empty $\kall[black]{k}{\kdot}$ cell. On the other hand, $\varphi'$ is the right hand side pattern of a reachability rule generated from a Hoare triple using transformation~\ref{transf}, so $\pi'_0$ also contains the empty $\kall[black]{k}{\kdot}$ cell. Moreover, program variables from both $\pi''_0$ and $\pi'_0$ are mapped to logical variables that are constrained by $\phi'' \land \bigwedge_{\sigma''}$, and $\phi' \land \bigwedge_{\sigma'}$, respectively. 
 Therefore, we can say that proving $\pi''_0 \land (\phi'' \land \bigwedge_{\sigma''}) \Rightarrow \pi'_0 \land (\phi' \land \bigwedge_{\sigma'})$ reduces to proving the implication $(\phi'' \land \bigwedge_{\sigma''}) \rightarrow (\phi' \land \bigwedge_{\sigma'})$. This implication holds if and only if $(\phi'' \land \bigwedge_{\sigma''} \land \neg(\phi' \land \bigwedge_{\sigma'}))$ is not satisfiable, or 
 {\it unsat}$(\phi'' \land \bigwedge_{\sigma''} \land \neg(\phi' \land \bigwedge_{\sigma'}))$ returns true. The {\it unsat} predicate checks if the formula is not satisfiable by making a call to the Z3 SMT solver. 
 
The semantics of \mytt{implies} is shown below:\vspace{1ex}
$
\fontsize{9}{11}
\selectfont
\kall[black]{k}{\reduce{\terminal{implies}(\kall[black]{cfg}{\kall[black]{k}{\kdot}\kall[black]{env}{E''}\kall[black]{cond}{\psi''})}}{\kdot}}
\kall[black]{env}{E'}\kall[black]{cond}{\phi'}\\
\hspace*{20ex}\mathtt{when}\text{ }{\mathit unsat}(\phi'' \land \bigwedge_{\sigma''} \land \neg(\phi' \land \bigwedge_{\sigma'}))
$~\vspace{2ex}


When instantiating the methodology on a language definition, one may need additional constructs for defining $\bigwedge_\sigma$. For \IMP, we have defined a function which traverses the state (i.e. the content of the $\kall[black]{env}{}$ cell) and returns a conjunction of equalities, which is then added to the path condition. 

\subsection{Proving \mytt{SUM}}

In the following, we are going to show how the enriched semantics of \IMP proves an annotated program. \mytt{SUM}, shown in Figure~\ref{sum}, computes the sum of the natural numbers up to a given \mytt{n}. When executed with the \K tool, the program is initially plugged into the $\kall[black]{k}{}$ cell of the configuration: $\kall[black]{k}{\mathtt{{\fontsize{8}{10}\selectfont SUM}}}\kall[black]{\!env\!}{\!.\!}\kall[black]{\!cond\!}{\!.\!}$. Then, the rewrite rules from the semantics of \IMP execute properly the program. After declaring variables, the configuration becomes:
$
\kall[black]{k}{\mathtt{\sm{PRE\text{ }POST\text{ }CODE}}}
\kall[black]{env}{\mathtt{S}\mapsto 0\text{ }\mathtt{i}\mapsto 0\text{ }\mathtt{n}\mapsto 0}\kall[black]{cond}{true}
$
The current program represents now a Hoare triple, having precondition, postcondition and \mytt{CODE} to execute. Therefore, we can apply the rule which transforms the triple into \mytt{assume \kra implies} sequence:
\[
\fontsize{8}{10}
\selectfont
\hspace{-1ex}\kall[black]{\!k\!}{\mathtt{assume(\!\kall[black]{\!k\!}{\sm{CODE}}\kall[black]{\!env\!}{\!\sigma\!}\kall[black]{\!cond\!}{\sm{PRE}})}\!\!\kra\!\! \mathtt{implies(\!\kall[black]{k}{\!\kdot\!}\kall[black]{\!env\!}{\!\sigma'\!}\kall[black]{\!cond\!}{\sm{POST}})}}\vspace{-1ex}
\]
\[
\kall[black]{env}{\mathtt{S}\mapsto 0\text{ }\mathtt{i}\mapsto 0\text{ }\mathtt{n}\mapsto 0}\kall[black]{cond}{true}\vspace{-1ex}
\]
Note that $\sigma$ and $\sigma'$ bind program variables to fresh symbolic values: $\sigma\eqbydef\mathtt{S}\mapsto \mathit{S}\text{ }\mathtt{i}\mapsto \mathit{i}\text{ }\mathtt{n}\mapsto \mathit{n}$ and $\sigma'\eqbydef\mathtt{S}\mapsto \mathit{S'}\text{ }\mathtt{i}\mapsto \mathit{i'}\text{ }\mathtt{n}\mapsto \mathit{n'}$. The code \mytt{CODE}, the precondition \mytt{PRE}, and the postcondition \mytt{POST} become part of a reachability rule according to transformation~\ref{transf}.\\
Since \mytt{assume} is now at the top of the $\kall[black]{k}{}$ cell, we can apply the corresponding rewrite rule, which loads the argument in the current configuration:~\vspace{-1ex}
\[
\fontsize{8}{10}
\selectfont
\hspace{-1ex}\kall[black]{k}{\mathtt{CODE}\!\kra\!\!\mathtt{implies(\!\kall[black]{k}{\!\kdot\!}\kall[black]{env}{\!\sigma'\!}\kall[black]{cond}{POST})}}\vspace{-2ex}
\]
\[
\kall[black]{env}{\mathtt{S}\mapsto \mathit{S}\text{ }\mathtt{i}\mapsto \mathit{i}\text{ }\mathtt{n}\mapsto \mathit{n}}\kall[black]{cond}{\mathtt{PRE}}~\vspace{-1ex}
\]

\noindent \mytt{CODE} is now in the $\kall[black]{k}{}$ cell while the precondition \mytt{PRE} is set to be the initial path condition. Since \mytt{CODE \eqbydef ASGN\text{ }LOOP} the (symbolic) execution continues applying the rewrite rules for assignment, which update the state:~\vspace{-1.5ex}

\[
\fontsize{8}{10}
\selectfont
\hspace{-1ex}\kall[black]{k}{\mathtt{LOOP}\!\kra\!\! \mathtt{implies(\!\kall[black]{k}{\!\kdot\!}\kall[black]{env}{\!\sigma'\!}\kall[black]{cond}{POST})}}\vspace{-2ex}
\]
\[
\kall[black]{env}{\mathtt{S}\mapsto 0\text{ }\mathtt{i}\mapsto 1\text{ }\mathtt{n}\mapsto \mathit{n}}\kall[black]{cond}{\mathtt{PRE}}~\vspace{-1ex}
\]

\noindent At this point the symbolic execution can take two different paths because both rewrite rules corresponding to the annotated \mytt{while} loop match the current configuration: assume the loop condition \mytt{B} and the invariant, and execute \mytt{BODY}, or continue outside \mytt{LOOP}. Thus, the symbolic execution framework explores both paths evolving to the following two configurations:
\[
\fontsize{7}{9}
\selectfont
\hspace{-1ex}\kall[black]{\!k}{\mathtt{assume(\!\kall[black]{\!k\!}{BODY}\kall[black]{\!env\!}{\!\sigma\!}\kall[black]{\!cond\!}{\!INV\!\land\!B})}\!\!\kra\!\! \mathtt{implies(\!\kall[black]{k}{\!\kdot\!}\kall[black]{\!env\!}{\!\sigma'\!}\kall[black]{\!cond\!}{\!INV\!})\!}}\vspace{-2ex}
\]
\[
\kall[black]{env}{\mathtt{S}\mapsto 0\text{ }\mathtt{i}\mapsto 1\text{ }\mathtt{n}\mapsto \mathit{n}}\kall[black]{\!cond}{\mathtt{INV\!\land\!\mathtt{i <= n}}}~\vspace{-1.5ex}
\]
and
\[
\fontsize{7}{9}
\selectfont
\hspace{-1ex}\kall[black]{k}{\kdot\!\kra\!\! \mathtt{implies(\!\kall[black]{k}{\!\kdot\!}\kall[black]{env}{\!\sigma'\!}\kall[black]{cond}{POST})}}\vspace{-2ex}
\]
\[
\kall[black]{env}{\mathtt{S}\mapsto 0\text{ }\mathtt{i}\mapsto 1\text{ }\mathtt{n}\mapsto \mathit{n}}\kall[black]{cond}{\mathtt{PRE\land \neg(\mathtt{i <= n})}}~\vspace{-1ex}
\]
\noindent In the second configuration, the execution continues with $\mathtt{implies(\!\kall[black]{k}{\!\kdot\!}\kall[black]{env}{\!\sigma'\!}\kall[black]{cond}{POST})}$. The corresponding rewrite rules makes a call to the Z3 SMT solver for checking the satisfiability of $\phi'' \land \bigwedge_{\sigma''} \land \neg(\phi' \land \bigwedge_{\sigma'})$. In our case, the formula is $(\mathtt{PRE}\land \neg(\mathtt{i <= n}) \land \mathtt{n} = {\mathit n} \land \mathtt{i} = {\mathit 1} \land \mathtt{S} = {\mathit 0}) \land \neg(\mathtt{POST} \land  \mathtt{n} = {\mathit n'} \land \mathtt{i} = {\mathit i'} \land \mathtt{S} = {\mathit S'})$. If we replace the code macros \mytt{PRE} and \mytt{POST}, it becomes $(\mathtt{0 <= n}\land \neg(\mathtt{i <= n}) \land \mathtt{n} = {\mathit n} \land \mathtt{i} = {\mathit 1} \land \mathtt{S} = {\mathit 0}) \land \neg(\mathtt{S==n*(n+1)/2} \land  \mathtt{n} = {\mathit n'} \land \mathtt{i} = {\mathit i'} \land \mathtt{S} = {\mathit S'})$. Next, we can simplify it such that we get rid of program variables as follows: $(\mathtt{0 <=}{\mathit n}\land \mathtt{{\mathit n} < 1}) \land \neg(\mathtt{0=={\mathit n}*({\mathit n}+1)/2} \land  {\mathit n} = {\mathit n'} \land 1 = {\mathit i'} \land 0 = {\mathit S'})$. Obviously, $n=0$, which makes the formula unsatisfiable. So, the rewrite rule for $\mathtt{implies}$ is applied and the verification succeeds  on this execution path.

The other configuration still contains code which has to be executed. The \mytt{assume} executes as expected, setting  \mytt{BODY} as the content of the $\kall[black]{k}{}$ cell and updating the state. \mytt{BODY} updates the state new values for \mytt{S} and \mytt{n}:~\vspace{-1.5ex}
%\[
%\fontsize{9}{11}
%\selectfont
%\hspace{-1ex}\kall[black]{\!k}{\mathtt{BODY}\!\kra\!\! \mathtt{implies(\!\kall[black]{k}{\!\kdot\!}\kall[black]{\!env\!}{\!\sigma'\!}\kall[black]{\!cond\!}{\!INV\!})}}\vspace{-1ex}
%\]
%\[
%\kall[black]{env}{\mathtt{S}\mapsto {\mathit S + i}\text{ }\mathtt{i}\mapsto {\mathit i + 1}\text{ }\mathtt{n}\mapsto \mathit{n}}\kall[black]{cond}{\mathtt{INV \land \mathtt{i <= n}}}
%\]
\[
\fontsize{8}{10}
\selectfont
\hspace{-1ex}\kall[black]{\!k}{\mathtt{implies(\!\kall[black]{k}{\!\kdot\!}\kall[black]{\!env\!}{\!\sigma'\!}\kall[black]{\!cond\!}{\!INV\!})}}\vspace{-2ex}
\]
\[
\kall[black]{env}{\mathtt{S}\mapsto {\mathit S + i}\text{ }\mathtt{i}\mapsto {\mathit i + 1}\text{ }\mathtt{n}\mapsto \mathit{n}}\kall[black]{cond}{\mathtt{INV \land \mathtt{i <= n}}}~\vspace{-1ex}
\]

\noindent When executing $\mathtt{implies(\!\kall[black]{k}{\!\kdot\!}\kall[black]{\!env\!}{\!\sigma'\!}\kall[black]{\!cond\!}{\!INV\!})}$ we call again the SMT solver, but this time on a different formula $(\mathtt{INV}\land (\mathtt{i <= n}) \land \mathtt{n} = {\mathit n} \land \mathtt{i} = {\mathit i + 1} \land \mathtt{S} = {\mathit S + i}) \land \neg(\mathtt{INV} \land  \mathtt{n} = {\mathit n'} \land \mathtt{i} = {\mathit i'} \land \mathtt{S} = {\mathit S'})$. After simplification, the formula ${\mathit S==i*(i-1)/2}\land ({\mathit i <= n}) \land \neg({\mathit S==i*(i-1)/2 \land i<=n+1} \land  {\mathit n' = n} \land {\mathit i' = i + 1} \land {\mathit S' = S + 1})$ is proved unsatisfiable by the SMT solver. Since in both cases the verification succeeded we proved that \mytt{SUM} is correct w.r.t. given specification.

\begin{figure}
\centering
\begin{tabular}{| l | l |}
\hline
\begin{minipage}{.45\linewidth}
\begin{tabular}{l l l}
\hspace{-1.5ex}\mytt{PRE} & \hspace{-2ex}$\eqbydef$ & \hspace{-1.5ex}\mytt{0 <= n}\\
\hspace{-1.5ex}\mytt{POST} & \hspace{-2ex}$\eqbydef$ & \hspace{-1.5ex}\mytt{S==n*(n+1)/2}\\
\hspace{-1.5ex}\mytt{DECL} & \hspace{-2ex}$\eqbydef$ & \hspace{-1.5ex}\mytt{int\text{ }S, i, n;}\\
\hspace{-1.5ex}\mytt{ASGN} & \hspace{-2ex}$\eqbydef$ & \hspace{-1.5ex}\mytt{S = 0;i = 1;}\\
%\hspace{-1.5ex}\mytt{ASGN_1} & $\eqbydef$ & \mytt{i = 1;}\\
\hspace{-1.5ex}\mytt{BODY} & \hspace{-2ex}$\eqbydef$ & \hspace{-1.5ex}\mytt{S = S + i;}\mytt{i = i + 1;}\\
\hspace{-1.5ex}\mytt{INV} & \hspace{-2ex}$\eqbydef$ & \hspace{-1.5ex}\mytt{S==i*(i-1)/2}\\ & & \hspace{-1.5ex}\verb^&^\!\verb^&^\text{ }\mytt{i<=n+1}\\
\hspace{-1.5ex}\mytt{LOOP} & \hspace{-2ex}$\eqbydef$ & \hspace{-1.5ex}\mytt{while(i <= n)}\\ && \hspace{-1.5ex}\mytt{inv: POST} \mytt{\{BODY\}} \\
\hspace{-1.5ex}\mytt{CODE} & \hspace{-2ex}$\eqbydef$ & \hspace{-1.5ex}\mytt{ASGN\text{ }LOOP}\\
\hspace{-1.5ex}\mytt{SUM} & \hspace{-2ex}$\eqbydef$ & \hspace{-1.5ex}\mytt{DECL\text{ }PRE\text{ }POST\text{ }CODE}\\
\end{tabular}
\end{minipage}
&
\begin{minipage}{.4\linewidth}
\fontsize{9}{11}
\selectfont
\begin{alltt}
int S, i, n;
pre: 0<=n
post: S==n*(n+1)/2
S = 0; 
i = 1;
while(i <= n)
  inv: S==i*(i-1)/2 
          && i<=n+1
\{
  S = S + i;
  i = i + 1;
\}
\end{alltt}
\end{minipage}
~\\\hline
\end{tabular}
\caption{\label{sum} Code macros (left) and an annotated \IMP program \mytt{SUM} (right)~\vspace{-3ex}}
\end{figure}



\subsection{\IMP-Hoare}

We applied our methodology on the \K definition of \IMP. Then, we used the \K semantics compiler to generate an interpreter for annotated \IMP programs, thus, transforming the \K runner into a verifier for \IMP (\IMP-Hoare). We successfully tested our generated tool against the Key-Hoare tests suite. As we can observe in Table~\ref{tbl} the verification time of an annotated program using our generated tool is significantly bigger than the time Key-Hoare takes to verify the same program. The reason is that \K generated interpreters are based on the operational semantics, so they are not fast in general. For instance, running \mytt{arraySort} normally (without annotations) takes around 3.12 seconds, while verification of the same programs is done in approximatively 3.98 seconds. On the other hand, we can observe that for complex programs, the verification time using \IMP-Hoare does not increases as fast as when using KeY-Hoare. For instance, the ratio of the verification time for \mytt{arraySort} and the verification time for \mytt{arraySwap} is 9 when using KeY-Hoare, while for \IMP-Hoare the ratio is less than 2.

We also compared \IMP-Hoare with Spec\#, which is an object-oriented .NET programming language with design-by-contract features for method pre/postconditions, object invariants and also a non-null type system. We were interested in this comparison because Spec\# uses the Z3 SMT solver, the same as \IMP-Hoare. As we can observe there are no significant differences between the verification times when using the two tools. However, in the case of Spec\#, we need to mention that programs were enriched with Spec\# specific annotations such that they can be proved without warnings (non-null reference to array and non-null array elements).

There are at least two advantages that tools created using our methodology (e.g. \IMP-Hoare) have over KeY-Hoare and Spec\#. First, because our methodology is parametric in the \K definition of a language, the tools become modular (e.g.\IMP can be extended with new features directly in \IMP-Hoare without any changes). Second, the methodology is language independent, goal which is not achieved by any of the mentioned tools.
\vspace{2ex}
\begin{table}
\renewcommand\thetable{I}
\centering
\begin{tabular}{| l | c | c | c |}
\hline
\hline
Programs & \IMP-Hoare & Key-Hoare & Spec\#\\
% & verif. time (sec.) &  verif. time (sec.) \\ 
\hline\hline
%\hline
\mytt{arraySort}&3.98&0.90&4.40\\
\mytt{arraySwap}&2.78&0.10&3.17\\
\mytt{countdown}&3.06&0.10&2.57\\
\mytt{countdownExecutionTime}&2.83&0.10&2.63\\
\mytt{countdownTotal}&2.87&0.10&2.13\\
\mytt{delta\_solutions}&3.25&0.10&3.05\\
\mytt{gcd}&3.13&0.30&2.82\\
\mytt{integer\_division}&3.70&0.20&3.45\\
\mytt{max}&2.82&0.02&2.80\\
\mytt{multiplication}&3.35&0.20&3.12\\
\hline\hline
\end{tabular}
\caption{\IMP-Hoare vs. KeY-Hoare. The first column contains the programs from the KeY-Hoare tests suite, and last three columns contain the verification time (in seconds) for each program when verified with \IMP-Hoare, KeY-Hoare, and Spec\#, respectively.~\vspace{-2ex}}
\label{tbl}
\end{table}

\section{Related work}
\label{sec:comparison}

The work presented here was inspired from~\cite{Gordon10}, where the authors present methods for proving Hoare formulas based both on the forward computation of postconditions and on the backwards computation of preconditions. Even if computing the weakest precondition is simpler than computing the strongest postconditions, there are cases where the strongest postconditions computed using symbolic execution are useful (e.g. testing, model-checking). A Hoare triple can be verified by symbolically executing separate paths and combining the results. In some sense, our methodology follows the same approach: we first perform symbolic execution on an annotated program (with precondition, postcondition and invariants),  and then we verify if the conjunction between the precondition and the collected path condition implies the postcondition. If the implication holds for all the program paths, then the program is proved correct.

%As pointed in the introduction, the main disadvantage of the Hoare Logic is that the deduction system depends on the language syntax. For this reason, most of the existent implementations of Hoare Logic deductive system are limited to a single language. There are many tools that use Hoare Logic for reasoning (e.g. \cite{Key-Hoare}, \cite{DBLP:conf/arith/BoldoF07}, \cite{ITS}, \cite{JAlgo}, \cite{Sasse:2007:JVT:1279349.1279449} but there are only a few based on the language semantics. An interesting approach, which uses compositional natural semantics and Hoare Logic for reasoning about low level programming languages has been proposed in~\cite{Saabas05acompositional}. Another tool based on semantics is Java+ITP~\cite{Sasse:2007:JVT:1279349.1279449}. It is based on  an algebraic continuation passing style (CPS) semantics for a fragment of the Java language. After being decomposed, Hoare triples are translated into semantically equivalent first-order verification conditions (VCs) which are then sent to Maude's Inductive Theorem Prover (ITP) to be discharged. The long-term goal of this project is to use extensible and modular rewriting logic semantics of programming languages to create a generic framework for developing program verification tools.\vspace{2ex}

\section{Conclusions and Future work}
\label{sec:conclusions}

We have presented a generic methodology for transforming the operational semantics of a language, given as a set of rewrite rules, into another semantics, which is used to generate a Hoare Logic verifier for that language. It is based on the theoretical results proved in ~\cite{rosu-stefanescu-2012-fm}, and on Theorem~\ref{th}, which proves that symbolic execution derives a set of reachability rules. Hoare triples are transformed into reachability rules and proved using symbolic execution and the Z3 SMT solver.  We have instantiated our methodology of \IMP. We used the additional constructs \mytt{assume} and \mytt{implies} to prove reachability rules, and we enriched the language with syntax for preconditions, postconditions, and invariants. Next, we provided rewrite rules which transform Hoare triples into reachability rules. Once the steps of the methodology have been applied, we generated a verifier for \IMP annotated programs. The generated tool was tested successfully against the KeY-Hoare tests suite.

{\bf Future work}. The most important result presented in this paper is that the symbolic execution we proposed in~\cite{arusoaie:hal-00766220} derives a valid set of reachability rules. We were able to verify Hoare triples because these are particular cases of reachability rules. As a future work, we want to improve our symbolic execution framework, such that it can be used to develop verifiers using the language independent Matching Logic reachability deduction system~\cite{rosu-stefanescu-2012-fm}, or other logics for reasoning about programs (e.g. Separation Logic~\cite{DBLP:conf/lics/Reynolds02}).
More generally, our symbolic execution can be used for program testing, debugging, and verification, but with the added value of being language independent and grounded in formal operational semantics. In order to achieve that, we have to develop a rich domain of symbolic values, able to handle e.g., heaps, stacks, and other common data types.~\vspace{-.5ex}
% use section* for acknowledgement
\section*{Acknowledgment}

The results presented in this paper would not have been possible without effective advices of Prof. Dr. Dorel Lucanu. 
% We want to especially thank him for his efforts and fruitful ideas. 
Also, the work presented here is supported by Contract 161/15.06.2010, SMIS-CSNR 602-12516 (DAK).
%\newpage

%\tbd{De revazut citarile: apare hoare cu litera mica (trebuie scris {H}oare), itp, etc.}



% trigger a \newpage just before the given reference
% number - used to balance the columns on the last page
% adjust value as needed - may need to be readjusted if
% the document is modified later
%\IEEEtriggeratref{8}
% The "triggered" command can be changed if desired:
%\IEEEtriggercmd{\enlargethispage{-5in}}

% references section

% can use a bibliography generated by BibTeX as a .bbl file
% BibTeX documentation can be easily obtained at:
% http://www.ctan.org/tex-archive/biblio/bibtex/contrib/doc/
% The IEEEtran BibTeX style support page is at:
% http://www.michaelshell.org/tex/ieeetran/bibtex/
\bibliographystyle{IEEEtran}
% argument is your BibTeX string definitions and bibliography database(s)
%\bibliography{IEEEabrv,../bib/paper}
%
% <OR> manually copy in the resultant .bbl file
% set second argument of \begin to the number of references
% (used to reserve space for the reference number labels box)
%\begin{thebibliography}{1}

%\bibitem{IEEEhowto:kopka}
%H.~Kopka and P.~W. Daly, \emph{A Guide to \LaTeX}, 3rd~ed.\hskip 1em plus
%  0.5em minus 0.4em\relax Harlow, England: Addison-Wesley, 1999.
%
%
%\end{thebibliography}
%\bibliographystyle{amsplain}
\bibliography{references}





% that's all folks
\end{document}


